There Is No Preview Available For This Item
This item does not appear to have any files that can be experienced on Archive.org.
Please download files in this item to interact with them on your computer.
Show all files
Separation logic is a promising new approach to modular reasoning, but so far it has primarily been applied to low-level C-like languages. To extend separation logic to allow modular reasoning about object-oriented languages like Java, we must add encapsulation and behavioural subtyping to the logic. However, a naive integration of behavioural subtyping and separation logic is too restrictive. In this talk I will demonstrate how abstract predicate families provide an abstraction mechanism that addresses these restrictions, by mirroring dynamic dispatch in the logic. We demonstrate the utility of our approach with a series of examples, including the Visitor pattern.